Verify Crab's inferred invariants with Lean - #18

Adds --verify-with-lean: after the analysis, export the CFG and the
invariants to JSON, and ask a Lean 4 development to prove them sound.
The JSON is the whole interface between the two sides.

Only the roots of the call graph are checked. A callee's invariants are
conditional on its call sites, while the theorem Lean proves quantifies
over every initial state, so checking one in isolation would ask a
stronger question than Crab answered.

A failure is reported as "could not verify", never as a claim about the
analysis: it may only mean the proof search was too weak. Where the
arithmetic ran out, the assignment it could not rule out is shown in the
program's own variables.

Enabled by configuring with -DLAKE_EXECUTABLE.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Extends the Lean development from the integer core to the whole boolean
fragment: bool_assign_cst, bool_assign_var, bool_binop, bool_assume,
bool_assert and bool_select.

Representation. `State` gains a separate `bools : Var -> Bool` store rather
than encoding booleans as 0/1 integers, and `Assn`'s conjuncts become an
`Atom` sum (`.lin` / `.bool`). Crab exports boolean facts as 0/1 linear
constraints, but measured across int, int-terms, int-set, zones, oct-snf and
pk, a bool-tagged constraint is always `1*b = 0` or `1*b = 1` -- never
relational -- because Crab's booleans go through a flat per-variable lattice.
The uniform encoding would therefore buy nothing while costing `and` as a
multiplication and requiring a type environment to confine a havoc'd boolean
to {0,1}. The reader refuses any other bool-tagged shape by name. Rationale
in full in Crabber/Syntax.lean.

No boolean statement introduces a quantifier, so goals stay quantifier-free
and booleans never reach omega: `LinCon.check` turns a recorded comparison
back into the proposition it decided, and simp's Bool lemmas do the rest.

Assertion safety. `AssertFails` now quantifies over an arbitrary statement
via `Stmt.obligation` instead of naming `Stmt.assert`. This is forced, not
cosmetic: a program whose assertions are all boolean would otherwise have
`not AssertFails` proved vacuously, reading as "no assertion can fail" while
quantifying over none of them. Every constructor is listed explicitly so a
future assert-like statement is a missing-cases error rather than a silent
`True`.

`chk` is now derived, not generated. `wpStmt` already puts an assert's
obligation inside its block's verification condition, so `wp_split` extracts
it and `chk_of_VC` supplies what `assert_safe` wants. `verified` takes two
hypotheses instead of three and `crab_verify` no longer emits a per-program
`chk` proof. This rests on the `and` reading of assert; see the note in
Crabber/Samples/Test1Foo.lean for what switching to `->` would cost.

samples/test-bool-1.crabir is the new end-to-end sample -- cast-free, unlike
test-6, which reaches its booleans through trunc and stays out of scope. Its
`safe` cfg proves; its `unsafe` companion has its failing block's VC refuted
rather than merely left unproved.

Also fixes a cross-language coupling this change broke: lean_verify.cpp
classifies "not attempted" by substring-searching Lean's error text, and
rewording the reader's refusal silently downgraded test-6, test-8, test-10
and the test-call-* samples to "could not verify" with a green build. Both
ends now agree on one phrase, and the contract is commented at both.

Full sample suite verified unchanged against the pre-change baseline.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>